Nuprl Lemma : increasing_inj
4,23
postcript
pdf
k
,
m
:
,
f
:(
k
m
). increasing(
f
;
k
)
Inj(
k
;
m
;
f
)
latex
Definitions
Inj(
A
;
B
;
f
)
,
T
,
True
,
i
j
<
k
,
A
B
,
P
&
Q
,
A
,
False
,
P
Q
,
Prop
,
increasing(
f
;
k
)
,
S
T
,
S
T
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
t
T
,
,
{
T
}
,
Dec(
P
)
,
P
Q
Lemmas
decidable
lt
,
increasing
implies
,
nat
wf
,
int
seg
wf
,
increasing
wf
origin
k, m:
, f:(k
m). increasing(f;k) 
Inj(k; m; f) k, m:, f:(km). increasing(f;k) Inj(k; m; f) 
T
j < kB
A Q
T
T
}x:A. B(x)
T
Q